the_w:World, e:E. val(e)  V(loc(e);kind(e)) 

latex

Definitions	x:A. B(x), t  T, valtype(i;a), V(i;k), kind(e), w.TA, w.M, val(e), P  Q, Prop
Lemmas	w-val wf, w-loc wf, w-act wf, w-action wf, not wf, assert wf, w-isnull wf, w-act-not-null, w-E wf, world wf